/* Benchmarks for the PionterC verifier. */

// list

struct list
{
  int data;
  struct list* next;
};

/*@ Pi= {{p}}*/
int f(int* p)
{
  int i;
  struct list* w, x, y, z;
  
  //w = alloc(struct list);
  //x = alloc(struct list);
  //y = alloc(struct list);
  //z = alloc(struct list);
  w->data = 1;
  w->next = x;
  x->data = 2;
  x->next = y;
  y->data = 3;
  y->next = z;
  z->data = 4;
  z->next = null;
  i = w->next->next->next->data;
  return i;
}
/*@  result==4 */